$\forall$${\it es}$:ES, $i$:Id, $P$:(\{$e$:E$\mid$ loc($e$) $=$ $i$ \}$\rightarrow$Prop).
\\[0ex]$\forall$$e$@$i$. $P$($e$) $\Leftrightarrow$ $\forall$$e$@$i$. first($e$) $\Rightarrow$ $P$($e$) \& $\forall$$e$@$i$. $\neg$first($e$) $\Rightarrow$ $P$(pred($e$)) $\Rightarrow$ $P$($e$)